M1, M2:MsgA.
M1  M2
 (k:Knd, l:IdLnk, s:M2.state, v:M2.da(k), i:Id,
 (ms:(tg:Idif source(l) = i M2.da(rcv(l,tg)) else Top fi) List.
 (M2.send(k;l;s;v;ms;i)  M1.send(k;l;s;v;ms;i)) 

latex

Definitions

f  g, S  T, P  Q, SQType(T), {T}, x  dom(f), product-deq(A;B;a;b), KindDeq, IdLnkDeq, concat(ll), map(f;as), f(x), a:A fp B(a), State(ds), 1of(t), 2of(t), x. t(x), f(x)?z, False, Knd, IdLnk, Id, if b t else f fi, rcv(l,tg), Top, M.send(k;l;s;v;ms;i), M.da(a), M.state, M1  M2, MsgA, Valtype(da;k), A & B, z != f(x)  P(a;z), Unit, P  Q, P & Q, P  Q, a = b, source(l), , Prop, b, A, t  T, b, x:A. B(x)

Lemmas

assert wf, not wf, bnot wf, bool wf, lsrc wf, eq id wf, assert of bnot, eqff to assert, iff transitivity, eqtt to assert, top wf, rcv wf, ma-da wf, ifthenelse wf, Id wf, ma-st wf, IdLnk wf, Knd wf, ma-sub wf, msga wf, pi2 wf, fpf-cap wf, pi1 wf, ma-state wf, fpf-trivial-subtype-top, fpf-ap wf, map wf, concat wf, idlnk-deq wf, Kind-deq wf, product-deq wf, fpf-dom wf, bool sq, bool cases, subtype-fpf-cap-top, fpf-cap-void-subtype